Nuprl Definition : R-self-interface
11,40
postcript
pdf
R-self-interface(
R
)
== es_realizer_ind(
R
;
== es_realizer_ind(
True;
== es_realizer_ind(
left
,
right
,
rec1
,
rec2
.(
rec1
rec2
);
== es_realizer_ind(
loc
,
T
,
x
,
v
.True;
== es_realizer_ind(
loc
,
T
,
x
,
L
.True;
== es_realizer_ind(
lnk
,
tag
,
L
.True;
== es_realizer_ind(
loc
,
ds
,
knd
,
T
,
x
,
f
.True;
== es_realizer_ind(
ds
,
knd
,
T
,
l
,
dt
,
g
.((
isrcv(
knd
))
== es_realizer_ind(
(lnk(
knd
) =
l
)
== es_realizer_ind(
subtype_rel(fpf-cap(
dt
; id-deq; tag(
knd
); void);
T
));
== es_realizer_ind(
loc
,
ds
,
a
,
T
,
P
.True;
== es_realizer_ind(
loc
,
k
,
L
.True;
== es_realizer_ind(
loc
,
k
,
L
.True;
== es_realizer_ind(
loc
,
x
,
L
.True)
latex
clarification:
R-self-interface(
R
)
== es_realizer_ind(
R
;
== es_realizer_ind(
True;
== es_realizer_ind(
left
,
right
,
rec1
,
rec2
.(
rec1
rec2
);
== es_realizer_ind(
loc
,
T
,
x
,
v
.True;
== es_realizer_ind(
loc
,
T
,
x
,
L
.True;
== es_realizer_ind(
lnk
,
tag
,
L
.True;
== es_realizer_ind(
loc
,
ds
,
knd
,
T
,
x
,
f
.True;
== es_realizer_ind(
ds
,
knd
,
T
,
l
,
dt
,
g
.((
isrcv(
knd
))
== es_realizer_ind(
(lnk(
knd
) =
l
IdLnk)
== es_realizer_ind(
subtype_rel(fpf-cap(
dt
; id-deq; tag(
knd
); void);
T
));
== es_realizer_ind(
loc
,
ds
,
a
,
T
,
P
.True;
== es_realizer_ind(
loc
,
k
,
L
.True;
== es_realizer_ind(
loc
,
k
,
L
.True;
== es_realizer_ind(
loc
,
x
,
L
.True)
latex
Definitions
es
realizer
ind
,
P
Q
,
b
,
isrcv(
k
)
,
P
Q
,
s
=
t
,
IdLnk
,
lnk(
k
)
,
fpf-cap(
f
;
eq
;
x
;
z
)
,
id-deq
,
tag(
k
)
,
void
,
True
FDL editor aliases
R-self-interface
origin